\begin{tabbing}
$\forall$${\it es}$:ES, $L$:(Id List).
\\[0ex]fischer($L$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E, $j$:Id.\+
\\[0ex]Newround($e$)
\\[0ex]$\Rightarrow$ ($j$ $\in$ $L$)
\\[0ex]$\Rightarrow$ ($\neg$($j$ = loc($e$)))
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$:E.\+
\\[0ex]($\uparrow$isrcv(${\it e'}$))
\\[0ex]$\Rightarrow$ (sender(${\it e'}$) = $e$)
\\[0ex]$\Rightarrow$ (loc(${\it e'}$) = $j$)
\\[0ex]$\Rightarrow$ (tag(${\it e'}$) = "free" $\in$ Id)
\\[0ex]$\Rightarrow$ (lnk(${\it e'}$) = $<$loc($e$), $j$, "z"$>$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ the rcv(free message from $e$ to $j$) $\leq$loc ${\it e'}$ ))
\-\-
\end{tabbing}